a:, n:. Rem(a;n;a rem n) 

latex

Up	int 2, int 2
Definitions	t  T, Rem(a;n;r), x:A. B(x), False, P  Q, A, a  b  T , , P & Q, x:A. B(x), A  B, , , S  T
Lemmas	nat wf, nat plus wf, div nrel wf, divide wf, div fun sat div nrel, nat plus inc int nzero, div rem sum